\section{The Type System}\label{s:types}
Our type discipline builds upon the one given in~\cite{DBLP:conf/ppdp/GarraldaCD06}.
As such, the type syntax is divided into three categories: \emph{basic types}, which  handle expressions; 
\emph{pre-session types} describing a channel's ability for sending/receiving messages and offering/selecting be\-hav\-iors; 
\emph{session types} representing well-formed session-typed be\-hav\-ior; and
\emph{channel types}, which can be a session type or a \emph{used session}~$\bot$. %this will be made clear later on).

We extend the judgments of~\cite{DBLP:conf/ppdp/GarraldaCD06} with an \emph{interface} $\Delta$---the collection of all session types declared in a given process. 
As we have seen, interfaces are key to the operational definition of update actions. 
To define the interface of processes with recursion, our 
session types are \emph{qualified}: they can be linear ($\qual$) or unrestricted ($\quau$). 
While $\qual$ is used for those session types to be used just once, 
$\quau$ annotates those session types intended to feature a persistent behavior---roughly, these
are types assigned to sessions declared in the context of a recursive process.
Formally, we have:
 
\begin{definition}\label{d:types}
 \emph{Basic types} ($\capab$), \emph{pre-session types} ($\zeta$), 
 \emph{session types} ($\rho_\qua$, $\sigma_q$), and
\emph{channel types} ($\omega$) are as in Table~\ref{tab:types}.
\begin{table}
\textsc{Types}
$$
\begin{array}{lclr}
\capab & ::= & \mathsf{int} \sepr \mathsf{bool} \sepr \dots ~~~& \text{basic types}\\
%\varphi & ::= & \var & \text{process variable \todo{are these used?}} \\
%\end{array}
%$$
%%Session Types 
%$$
%\begin{array}{lcll}
\zeta &\!\!\!\!::= & \epsilon \!\!\!\!\!\!& \text{closed session}\\
		& \sepr & \!\!\!\!\! !(\tilde{\capab}).\zeta \sepr ?(\tilde{\capab}).\zeta & \text{send, receive} \\ 
		& \sepr & \!\!\!\!\! !(\sigma).\zeta \sepr ?(\sigma).\zeta & \text{throw, catch} \\ 
		& \sepr & \!\!\!\!\! t & \text{type variable} \\ 
		& \sepr & \!\!\!\!\! \mu t.\zeta & \text{recursive type} \\ 
		& \sepr & \!\!\!\!\! \&\{n_1:\zeta_1, \dots,  n_k:\zeta_k \}  \quad &  \text{branch} \\
		& \sepr & \!\!\!\!\! \oplus\{n_1:\zeta_1, \dots , n_k:\zeta_k \}  &  \text{select} \vspace{0.5mm} \\
\rho & \triangleq & \!\!\!\!\ \{ \zeta ~|~ \mathsf{ftv}(\zeta) = \emptyset\} & \text{} \vspace{0.5mm}\\
\qua &\!\!\!\!::= & \!\!\!\qual \sepr \quau \!\!\!\!\!\!& \text{type qualifiers} \vspace{0.5mm} \\
%\end{array}
%. \\
%\begin{array}{lcll}
~\omega &::=& \rho_\qua & \text{session types}\\
	& \sepr &	\bot \quad& \text{used session}
\end{array}
$$
\textsc{Environments}
$$
\begin{array}{lclr}
\Delta &\!\!\!::= & \!\!\! \emptyset \sepr \Delta, \langle \rho, k \rangle & \text{process interface} \\
\Phi & ::= & \!\!\! \emptyset \sepr \Phi, c:\omega & \text{active sessions}\\
\Gamma &::= & \!\!\! \emptyset \sepr \Gamma, e:\capab & \text{first-order env.}\\
\Theta &::= & \!\!\! \emptyset \sepr \Theta, Y:\Phi{\cdot}\Delta \sepr \Theta,\mathsf{X}:\Delta & \text{higher-order env.}
\end{array}
$$  \vspace{-4mm}
\caption{Types and Typing Environments}\label{tab:types}
\end{table}
\end{definition}

Our type syntax contains the usual session types constructs, with 
their standard meanings. 
We use $t, t', \ldots$ to range over \emph{type variables}; also, we 
require recursive types to be \emph{contractive}, i.e., not 
containing a subexpression of the form $\mu t.\mu t_1.\cdots.\mu t_n.t$.
Binder $\mu$ gives rises to standard notions of free/bound type variables; 
$\mathsf{ftv}(\zeta)$ denotes the free type variables in $\zeta$.
We consider session types modulo folding/unfolding of recursive types.
%\todo{contractive types?}
We now introduce the central notion of  \emph{duality} for (pre-session) types.


\begin{definition}[duality]\label{d:dual}
Given a pre-session type $\zeta$, 
its \emph{dual}
(noted $\overline{\zeta}$) is inductively defined in Table~\ref{tab:dual}.
\begin{table}[t]
$$
\begin{array}{rcl}
 \overline{\epsilon} &\!\!=\! & \epsilon\\
 \overline{!(\tau).\zeta} &\!\!=\! & ?(\tau).\overline{\zeta} \text{~~(with $\tau = \tilde{\capab}$ or $\tau = \rho_\qua$)}\\
 \overline{?(\tau).\zeta} &\!\!=\! & !(\tau).\overline{\zeta} \text{\,~~(with $\tau = \tilde{\capab}$ or $\tau = \rho_\qua$)}\\
% \overline{?(\tau).\zeta} &\!\!=\! & !(\tilde{\capab}).\overline{\zeta}\\
% \overline{!(\sigma).\zeta} &\!\!=\! & ?(\sigma).\overline{\zeta}\\
% \overline{?(\sigma).\zeta} &\!\!=\! & !(\sigma).\overline{\zeta}\\
 \overline{t} &\!\!=\! & t \\
 \overline{\mu t.\zeta} &\!\!=\! & \mu t.\overline{\zeta}\\
 \overline{\&\{n_1:\zeta_1 , \ldots , n_k:\zeta_k \}} &\!\!=\! & \oplus\{n_1:\overline{\zeta_1} , \ldots , n_k:\overline{\zeta_k} \}\\
 \overline{ \oplus\{n_1:\zeta_1 , \ldots , n_k:\zeta_k \}} &\!\!=\!& \&\{n_1:\overline{\zeta_1} , \ldots , n_k:\overline{\zeta_k} \}
\end{array}
$$ \vspace{-4mm}
\caption{Dual of pre-session types}\label{tab:dual}
\end{table}
\end{definition}

%In order to type a process $P$ 
%We use two kinds of typing environments, noted $\Gamma$ and $\Theta$.
We comment on the typing environments defined in Table~\ref{tab:types}.
An interface $\Delta$ is a set of pairs $\langle \rho, k\rangle$ where $\rho$
is a session type and $k$ is either an integer $j > 0$ or $\infty$.
The intention is to capture the session types declared in a process,
the number of times a type is declared, and whether a type is 
%declared in the context of a recursive definition.
%\todo{I would substitute the above sentence with: and whether a type is 
linear or unrestricted.
In $\Delta$, types are recorded at most once; several occurrences of the same type are captured
by the second component of the pair. 
The union of an interface and a pair,
noted $\Delta \addelta \langle \rho, k\rangle$, is defined as follows:
$$
\Delta \addelta \langle \rho, k\rangle \!\triangleq \!\!
\begin{cases}
\Delta' \cup \{\langle \rho, k + j\rangle \} & \text{if } \exists\Delta'.  \Delta = \Delta' \cup \{\langle \rho, j\rangle \}	\\
\Delta \cup \{\langle \rho, k \rangle \} & \text{otherwise} 
\end{cases}
$$
Recall that $\infty + 1 = \infty$.
We sometimes write $\Delta \addelta \rho_\qua$ to stand 
for $\Delta \addelta\{\langle \rho, 1\rangle \}$ (if $\qua = \qual$) or
$\Delta \addelta \{\langle \rho, \infty\rangle \}$ (if $\qua = \quau$).
The extension of $\addelta$ from pairs $\langle \rho, k \rangle$ 
to interfaces (denoted $\Delta_1 \addelta \Delta_2$) is as expected.
Letting $\alpha$ stand for \emph{session prefixes} (expression/channel input and output, session selection and close), 
the interface of a process $P$, denoted $\intf{P}$, is inductively defined in Table~\ref{tab:int}.

\begin{table}[t]
$$
\intf{P} =  
\begin{cases}
\langle \rho,1 \rangle \addelta \intf{P'}& \text{if } P = \nopen{a}{c:\rho_\qual}.P'	\\
\langle \rho,\infty \rangle \addelta \intf{P'} & \text{if } P = \nopen{a}{c:\rho_\quau}.P'	\\
%\intf{P'}& \text{if } P =  \alpha.P'  \\
\intf{P'} & \text{if } P = \component{l}{h}{\Delta}{P'} \text{ or } P = \alpha.P' \\
\emptyset & \text{if } P = \updated{l}{X}{\Delta_1}{\Delta_2}{Q} \text{ or } P = \mathbf{0} \\
\intf{P_1} & \text{if } P = \ifte{e}{P_1}{P_2} \\
\Delta& \text{if } P = \rec{Y{:}\Phi{\cdot}\Delta}{P'}\\	
\intf{P_1} \addelta \intf{P_2}\!\!\!\!& \text{if } P = P_1 \parallel P_2 \\	 
\biguplus_i(\intf{P_i}) & \text{if } P = \branch{c}{n_1{:}P_1, \ldots, n_k{:}P_k} \\
\intf{P'} & \text{if } P = \restr{c}{P'} 
%\emptyset  & \text{if } 	P = \mathbf{0}  \\
\end{cases}
\vspace{-4mm}
$$
\caption{Interface of a process $P$}\label{tab:int}
\end{table}

Set $\Phi$ collects information on already active sessions: it records 
a channel name %on which the communication is taking place and the 
and its associated session type. % $\rho$ associated to the channel.  
While $\Gamma$ is a first-order environment which maps expressions with basic types $\capab$,
the higher-order environment $\Theta$ stores the type of process/recursion variables.
%%\todo{Add here that we consider update variables $\mathsf{X}$ and recursion variables $X$; we use $\mathcal{X}$ to refer to one of them.}
%The type of a process is divided into two parts, noted $\Phi$ and $\Delta = \Delta_l \shortmid \Delta_u$, resp.
%
%We use $\Delta_l \shortmid \Delta_u $ to denote information on the interface: i.e., what sessions can be established along the evolution of a process. This notation is intended to distinguish between \emph{linear} and \emph{unrestricted} sessions:
%while the set $\Delta_u$ will contain all those sessions which are in the scope of a recursion operator, 
%all the other sessions are linear and thus accumulated in the multiset $\Delta_l$. 
%
%We assume an operator $\addelta$ which adds sessions to  $\Delta_u$ and  $\Delta_l$ depending on the nature of each zone:  
%an unrestricted session is added only if it is not already present, 
%while a linear session is always added (as it is a multiset). 
%Dually, operator $\midelta$ is used to remove sessions from $\Delta_u$ and  $\Delta_l$: 
%while a removal from $\Delta_u$ has no effect, we write $\Delta_u \midelta \rho$ to denote the removal of one occurrence of session $\rho$ from $\Delta_l$. 
%\todo{Q: These operators are defined over sessions or over sets of sessions??}
%In what follows, to simplify the notation, we often write $\Delta$ to stand for $\Delta_l \shortmid \Delta_u $.
%Here we present the type system for our process language.
Given these environments, a \emph{type judgment} is  of form
$$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi}{\Delta}} $$ 
meaning that, under environments $\Gamma$ and $\Theta$, 
process $P$ has active sessions declared in $\Phi$ and interface %(a collection of not yet open sessions) 
$\Delta$. We then have:

\begin{definition}%[Well-typed process]
A process is well-typed if it can be typed using the rules in Tables \ref{tab:pitype} and~\ref{tab:session}.

\begin{table}[t]

$$
\begin{array}{cr}

\cfrac{}{\Gamma \vdash e:\capab} & \rulename{t:Exp} \\

\cfrac{}{\Gamma, x:\capab \vdash x:\capab} & \rulename{t:NVar} \vspace{-1mm}\\

\cfrac{}{\Gamma; \Theta,\mathsf{X}:\Delta \vdash \mathsf{X}:\type{\emptyset}{\Delta}}  & \rulename{t:PVar} \vspace{-1mm}\\

 \cfrac{}{\Gamma; \Theta,X:\Phi{\cdot}\Delta \vdash X:\type{\Phi}{\Delta}} &  \rulename{t:RVar} \vspace{2.5mm}\\


\cfrac{
\begin{array}{c}
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi, c:\rho_\qua}{\,\Delta}} 
%\mathsf{cond}(\Delta, \Delta_l, \Delta_u,  \Theta, \rho)
\end{array}
}{\judgebis{\env{\Gamma}{\Theta}}{\nopen{a}{c:\rho_\qua}.P}{ \type{\Phi}{\,\Delta \addelta \rho_\qua}}} & \rulename{t:Open} \vspace{2.5mm} 
\\





\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi, c:\rho}{ \Delta}} \qquad \Gamma \vdash \tilde{e}:\tilde{\capab}}{\judgebis{\env{\Gamma}{\Theta}}{\outC{c}{\tilde{e}}.P}{\type{\Phi, c:!(\tilde{\capab}).\rho}{ \Delta}}} & \rulename{t:Out}  \vspace{2.5mm}
\\


\cfrac{\judgebis{\env{\Gamma, \tilde{x}:\tilde{\capab}}{\Theta}}{P}{\type{\Phi, c:\rho}{\Delta}}}{\judgebis{\env{\Gamma}{\Theta}}{\inC{c}{\tilde{x}}.P }{\type{\Phi, c:?(\tilde{\capab}).\rho}{ \Delta}}} & \rulename{t:In} \vspace{2.5mm}
\\




\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi, c:\rho}{ \Delta}}}{\judgebis{\env{\Gamma}{\Theta}}{\throw{c}{d}.P}{\type{\Phi, c:!(\sigma).\rho, d:\sigma}{ \Delta}}} & \rulename{t:Thr} \vspace{2.5mm}
\\


\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi, c:\rho, d:\sigma}{\Delta}}}{\judgebis{\env{\Gamma}{\Theta}}{\catch{c}{d}.P }{\type{\Phi, c:?(\sigma).\rho}{ \Delta}}} & \rulename{t:Cat} \vspace{2.5mm}
\\

\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi}{\Delta}} \qquad h = \#\{c \mid c:\omega \in \Phi\} }{\judgebis{\env{\Gamma}{\Theta}}{\component{l}{h}{\Delta}{P} }{ \type{\Phi}{\Delta}}} &  \rulename{t:Loc}  \vspace{2.5mm}
\\

\cfrac{\judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\Delta_1}}}{P}{\type{\emptyset}{ \Delta_2 }}}{\judgebis{\env{\Gamma}{\Theta}}{\updated{l}{X}{\Delta_1}{\Delta_2}{P}}{\type{\emptyset}{ \emptyset}}} & \rulename{t:Upd}  \vspace{2.5mm}
\\ 

\cfrac{
\begin{array}{l}
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi_1}{ \Delta_1}} \\
 \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi_2}{ \Delta_2}}
\end{array}
 \quad 
\begin{array}{l}
\Phi = \Phi_1 \bowtie \Phi_2 \\ \Delta = \Delta_1 \addelta \Delta_2
\end{array}}{\judgebis{\env{\Gamma}{\Theta}}{P \parallel Q}{\type{\Phi}{\Delta}}} & \rulename{t:Par}  \vspace{2.5mm}
\\


\cfrac{ \judgebis{\env{\Gamma}{\Theta,Y:\Phi{\cdot}\Delta}}{ P}{\type{\Phi}{\Delta}}}{\judgebis{\env{\Gamma}{\Theta}}{\rec{Y:\Phi{\cdot}\Delta}{P}}{\type{\Phi}{\Delta}}} & \rulename{t:Rec} \vspace{2.5mm}
\\


 
 \cfrac{\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\Phi}{\Delta}} \qquad c\notin \dom{\Phi} }{\judgebis{\env{\Gamma}{\Theta}}{ \close{c}.P}{ \type{\Phi, c:\epsilon}{ \Delta}}} & \rulename{t:Clo}
\end{array}
$$  \vspace{-4mm}
\caption{Well-typed processes (I) }\label{tab:pitype}
\end{table}


\begin{table}[t]

$$
\begin{array}{cr}

\cfrac{}{\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}} & \rulename{t:Nil} \vspace{2.5mm}
\\

\cfrac{
\begin{array}{l}
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi}{\Delta}} \\ 
\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\Phi}{\Delta}}
\end{array}
 \quad 
 \Gamma \vdash e:\mathsf{bool} 
 }{\judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{\type{\Phi}{\Delta}}} & \rulename{t:If} 
 \vspace{2.5mm}
 \\
%\end{array}
%$$
%
%\caption{Well-typed located and update processes.}\label{tab:update}
%\end{table}
%
%
%\begin{table}[t]
%
%
%
%$$
%\begin{array}{cr}

%\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi, c:\rho}{ \Delta}} \quad \Delta' = \begin{cases}
%\Delta_u \addelta \rho & X \in \Theta\\
%\Delta_l \addelta \rho & \text{otherwise}
%\end{cases}
%}{\judgebis{\env{\Gamma}{\Theta}}{\open{c:\rho}.P}{ \type{\Phi}{\Delta'}}} & \rulename{Open}\\

\cfrac{\judgement{\Gamma}{\Theta}{P}{\Phi}{\Delta} \qquad c\notin \dom{\Phi} }{\judgement{\Gamma}{\Theta}{\restr{c}{P}}{\Phi}{\Delta}} & \rulename{t:Weak} \vspace{2.5mm}
\\

\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\Phi, c:\bot }{ \Delta}}}{\judgebis{\env{\Gamma}{\Theta}} {\restr{c}{P}}{\type{\Phi, c:\bot}{ \Delta}}} & \rulename{t:CRes} \vspace{2.5mm}
\\

\cfrac{
\begin{array}{c}
\forall i\in \{1,\ldots, k\}. \judgebis{\env{\Gamma}{\Theta}}{P_i}{\type{\Phi, c:\rho_i}{ \Delta}} \\
 \rho = \&\{n_1:\rho_1,\ldots, n_k:\rho_k \}
\end{array} 
 }{\judgebis{\env{\Gamma}{\Theta}}{\branch{c}{n_1:P_1, \ldots, n_k:P_k}}{\type{ \Phi, c:\rho}{ \Delta}}} & \rulename{t:Bra} \vspace{2.5mm}
\\

\cfrac{
\begin{array}{c}
\judgebis{ \env{\Gamma}{\Theta}}{P}{\type{\Phi, c:\rho_i}{ \Delta}} \quad 1 \leq i \leq k\\ 
\rho = \oplus\{n_1:\rho_1, \ldots , n_k:\rho_k \}
\end{array}
}{\judgebis{\env{\Gamma}{\Theta}}{\select{c}{n_i}.P}{\type{\Phi, c:\rho}{\Delta}}} & \rulename{t:Sel}
\end{array}  \vspace{-4mm}
$$
\caption{Well-typed processes (II)}\label{tab:session}
\end{table}
\end{definition}



%$$
%\omega_1 \bowtie \omega_2 = 
%\begin{cases}
%\bot & \text{if } \{\omega_1, \omega_2\} = \{ \rho , \overline{\rho}\}\\
%\text{undefined} & \text{otherwise}
%\end{cases}
%$$





We comment on some typing rules. %, starting with those rules which handle sessions (Table~\ref{tab:session}). 
Rule \rulename{t:Open} types the process $\nopen{a}{c:\rho_\qua}.P$. 
Observe how channel $c$
becomes bound and so it is removed from $\Phi$; 
simultaneously, 
$\Delta$ is extended with 
the now complete (non-active) session $\rho_\qua$.
%To enforce the distinction between $\Delta_u$ and $\Delta_l$ explained above, in 
%that rule,  $\mathsf{cond}(\Delta, \Delta_l, \Delta_u,  \Theta, \rho)$ stands for the predicate
%$(\exists X. X \in \dom{\Theta} \land \Delta = (\Delta_u \addelta \rho \shortmid \Delta_l)) \lor (\Delta = (\Delta_u \shortmid \Delta_l \addelta \rho))$.
%$(\Theta \neq \emptyset \land \Delta = (\Delta_u \addelta \rho \shortmid \Delta_l)) \lor (\Delta = (\Delta_u \shortmid \Delta_l \addelta \rho))$.
%Hence, if the session appears in the scope of a recursive operator (and so at least one recursion variable is declared in $\Theta$), then $\rho$ is added to  $\Delta_u$, otherwise it is inserted in $\Delta_l$.
Rule \rulename{t:Loc} checks that $h$ corresponds to the number of running sessions in $P$, i.e., the cardinality of $\Phi$.
Rule \rulename{t:Upd} requires that the type of $P(\mathsf{X})$ is $\Delta_2$ provided that $\mathsf{X}$ is of type ${\Delta_1}$. 
This way, the rule guarantees that the process resulting from an update action has the declared interfaces. 
%We also require that no active session is present in  $P(\mathsf{X})$.
%Finally, rules in Table \ref{tab:pitype}
%are used  to type  usual $\pi$-calculus and are standard. We comment only on 
Rule \rulename{t:Par} checks that only matching processes can be put in parallel. 
This is obtained via the \emph{merge operator} $\bowtie$, which ensures 
session type compatibility via duality:
%that if the same channel $c$ is used by two processes in parallel
%then their associated types must be dual to each other. %: i.e. $c:\rho$ and $c:\overline{\rho}$. In this case the channel is merged and its type becomes $c:\bot$, the type of a used session.
%More precisely, we have:


%Our type system makes use of the following auxiliary definitions, 
%formalizing type \emph{merge}:

\begin{definition}%[Merge]
We define 
$\omega_1 \bowtie \omega_2 = \bot$ if $\{\omega_1, \omega_2\} = \{ \rho , \overline{\rho}\}$
and $\omega_1 \bowtie \omega_2\,=\,\text{undefinded}$ otherwise. Then:
$$
\begin{array}{lcl}
\Phi_1 \bowtie \Phi_2 &\!\! =\!\!& \{ c:\omega_1 \bowtie \omega_2 \mid c:\omega_1 \in \Phi_1 \text{ and } c:\omega_2 \in \Phi_2\} \;\cup \\
&&\{ c:\omega_1 \mid c:\omega_1 \in \Phi_1 \text{ and } c\notin \dom{\Phi_2}\} \;\cup\\
&&\{ c:\omega_2 \mid c:\omega_2 \in \Phi_2 \text{ and } c\notin \dom{\Phi_1}\}
\end{array}
$$
\end{definition}
Rule \rulename{t:Close} extends $\Phi$ with a new channel with an empty session type. %whose associated session is still empty.
Rules \rulename{t:PVar} and \rulename{t:RVar} handle process and recursion variables, resp. %In both cases, they define an empty $\Phi$.
Rule \rulename{t:Weak} handles all those processes in which $\restr{c}{P} \equiv P$ holds, and %, i.e., where $c$ does not occur in $P$.
\rulename{t:CRes} types channel restriction (the expected rule for name restriction is elided).
%Rules in Table \ref{tab:update} are used to type adaptable processes and update actions. In particular, notice that 
While rules \rulename{t:Cat} and \rulename{t:Thr} handle delegation,
rules \rulename{t:In}, \rulename{t:Out},  
%\rulename{t:Cat}, \rulename{t:Thr},
\rulename{t:Bra},  and \rulename{t:Sel} are standard.
%they extend an existing session with the proper type.  

%\todo{dire che altre regole sono standard?}
%\todo{Rule \rulename{Rec} not sure what to write for rec}



%\section{Varius Comments}
%\begin{enumerate}
%	
%	\item pensare se il calcolo avrebbe piu' o meno senso, impedendo di eliminare locations	
%	
%	\item ATTENZIONE la regola \rulename{Loc red} crea un problema: se inclusa si rischia di non aggiornare le sessioni aperte al momento di una open (e simmetricamente di non chiuderle in caso di una close) questo comporta che in tutte le reduction rules ci si debba ricordare il nesting delle location fino a top level (ruolo di E), da questa osservazione deriva anche la giustificazione della definizione di nesting context
%	$$
%	\cfrac{P \pired P' }{\component{l}{n}{}{P} \pired \component{l}{n}{}{P'}} \qquad \rulename{Loc red}\\
%	$$
%
%	
%\end{enumerate}
